/*
 * Processor.h
 *
 *  Created on: Feb 10, 2010
 *      Author: anton.kuhlevskyi
 */

#pragma once

#include <memory>
#include "Nodes/Defs.h"

enum ProcessingType {CNF, DNF};

template<class Node, class NodeFactory >
class Processor
{
private:
	enum ProcessorAlgoSelector {CLASSIC , INPLASE};
	template<int _v>
	struct Int2Type
	{
		enum {value=_v};
	};

	NodeFactory & m_factory;
	ProcessingType m_type;

public:
	Processor(NodeFactory & factory, ProcessingType type = DNF)
		: m_factory(factory)
		, m_type(type)
	{}

private:
	/*
	 * Classic node Processor
	 */
	// ~(A & B) -> ~A | ~B
	inline bool MatchNotAnd(std::auto_ptr<Node> & nodeNot, Int2Type<CLASSIC> t)
	{
		// Check the passed node type
		if(NT_NOT != nodeNot->getNodeType())
			return false;

		// Check the child node type
		Node * nodeAnd = nodeNot->getChild(0);
		if(NT_AND != nodeAnd->getNodeType())
			return false;

		// Rewrite node
		Node * notA = m_factory.createNodeNot(nodeAnd->getChild(0)->clone());
		Node * notB = m_factory.createNodeNot(nodeAnd->getChild(1)->clone());
		nodeNot.reset(m_factory.createNodeOr(notA, notB));
		return true;
	}

	// ~(A | B) -> ~A & ~B
	inline bool MatchNotOr(std::auto_ptr<Node> & nodeNot, Int2Type<CLASSIC>)
	{
		// Check the passed node type
		if(NT_NOT != nodeNot->getNodeType())
			return false;

		// Check the child node type
		Node * nodeOr = nodeNot->getChild(0);
		if(NT_OR != nodeOr->getNodeType())
			return false;

		// Rewrite node
		Node * notA = m_factory.createNodeNot(nodeOr->getChild(0)->clone());
		Node * notB = m_factory.createNodeNot(nodeOr->getChild(1)->clone());
		nodeNot.reset(m_factory.createNodeAnd(notA, notB));
		return true;
	}

	// ~~A -> A
	inline bool MatchNotNot(std::auto_ptr<Node> & nodeNot, Int2Type<CLASSIC>)
	{
		// Check the passed node type
		if(NT_NOT != nodeNot->getNodeType())
			return false;

		// Check the child node type
		Node * child = nodeNot->getChild(0);
		if(NT_NOT != child->getNodeType())
			return false;

		// Rewrite node
		nodeNot.reset(child->getChild(0)->clone());
		return true;
	}

	// (A & B) | C -> (A & C) | (B & C)
	inline bool MatchOrAnd1(std::auto_ptr<Node> & nodeOr, Int2Type<CLASSIC>)
	{
		// Check the processing type
		if(DNF != m_type)
			return false;

		// Check the passed node type
		if(NT_OR != nodeOr->getNodeType())
			return false;

		// Check the child node type
		Node * nodeAnd = nodeOr->getChild(0);
		if(NT_AND != nodeAnd->getNodeType())
			return false;

		// Rewrite node
		Node * a = nodeAnd->getChild(0)->clone();
		Node * b = nodeAnd->getChild(1)->clone();
		Node * c1 = nodeOr->getChild(1)->clone();
		Node * c2 = nodeOr->getChild(1)->clone();

		Node * andAC = m_factory.createNodeAnd(a, c1);
		Node * andBC = m_factory.createNodeAnd(b, c2);
		nodeOr.reset(m_factory.createNodeOr(andAC, andBC));
		return true;
	}

	// A | (B & C) -> (A & B) | (A & C)
	inline bool MatchOrAnd2(std::auto_ptr<Node> & nodeOr, Int2Type<CLASSIC>)
	{
		// Check the processing type
		if(DNF != m_type)
			return false;

		// Check the passed node type
		if(NT_OR != nodeOr->getNodeType())
			return false;

		// Check the child node type
		Node * nodeAnd = nodeOr->getChild(1);
		if(NT_AND != nodeAnd->getNodeType())
			return false;

		// Rewrite node
		Node * a1 = nodeOr->getChild(0)->clone();
		Node * a2 = nodeOr->getChild(0)->clone();
		Node * b = nodeAnd->getChild(0)->clone();
		Node * c = nodeAnd->getChild(1)->clone();

		Node * andAB = m_factory.createNodeAnd(a1, b);
		Node * andAC = m_factory.createNodeAnd(a2, c);
		nodeOr.reset(m_factory.createNodeOr(andAB, andAC));
		return true;
	}

	// (A | B) & C -> (A | C) & (B | C)
	inline bool MatchAndOr1(std::auto_ptr<Node> & nodeAnd, Int2Type<CLASSIC>)
	{
		// Check the processing type
		if(CNF != m_type)
			return false;

		// Check the passed node type
		if(NT_AND != nodeAnd->getNodeType())
			return false;

		// Check the child node type
		Node * nodeOr = nodeAnd->getChild(0);
		if(NT_OR != nodeOr->getNodeType())
			return false;

		// Rewrite node
		Node * a = nodeOr->getChild(0)->clone();
		Node * b = nodeOr->getChild(1)->clone();
		Node * c1 = nodeAnd->getChild(1)->clone();
		Node * c2 = nodeAnd->getChild(1)->clone();

		Node * orAC = m_factory.createNodeOr(a, c1);
		Node * orBC = m_factory.createNodeOr(b, c2);
		nodeAnd.reset(m_factory.createNodeAnd(orAC, orBC));
		return true;
	}

	// A & (B | C) -> (A | B) | (A | C)
	inline bool MatchAndOr2(std::auto_ptr<Node> & nodeAnd, Int2Type<CLASSIC>)
	{
		// Check the processing type
		if(CNF != m_type)
			return false;

		// Check the passed node type
		if(NT_AND != nodeAnd->getNodeType())
			return false;

		// Check the child node type
		Node * nodeOr = nodeAnd->getChild(1);
		if(NT_OR != nodeOr->getNodeType())
			return false;

		// Rewrite node
		Node * a1 = nodeAnd->getChild(0)->clone();
		Node * a2 = nodeAnd->getChild(0)->clone();
		Node * b = nodeOr->getChild(0)->clone();
		Node * c = nodeOr->getChild(1)->clone();

		Node * orAB = m_factory.createNodeOr(a1, b);
		Node * orAC = m_factory.createNodeOr(a2, c);
		nodeAnd.reset(m_factory.createNodeAnd(orAB, orAC));
		return true;
	}

	/*
	 * Inplase node Processor
	 */
	// ~(A & B) -> ~A | ~B
	inline bool MatchNotAnd(std::auto_ptr<Node> & nodeNot, Int2Type<INPLASE>)
	{
		// Check the passed node type
		if (NT_NOT != nodeNot->getNodeType())
			return false;

		// Check the child node type
		Node * nodeAnd = nodeNot->getChild(0);
		if (NT_AND != nodeAnd->getNodeType())
			return false;

		Node * notA = m_factory.createNodeNot(nodeAnd->getChild(0));
		Node * notB = m_factory.createNodeNot(nodeAnd->getChild(1));
		nodeAnd->setChild(0, NULL);
		nodeAnd->setChild(1, NULL);

		nodeNot.reset(m_factory.createNodeOr(notA, notB));
		return true;
	}

	// ~(A | B) -> ~A & ~B
	inline bool MatchNotOr(std::auto_ptr<Node> & nodeNot, Int2Type<INPLASE>)
	{
		// Check the passed node type
		if(NT_NOT != nodeNot->getNodeType())
			return false;

		// Check the child node type
		Node * nodeOr = nodeNot->getChild(0);
		if(NT_OR != nodeOr->getNodeType())
			return false;

			// Rewrite node
		Node * notA = m_factory.createNodeNot(nodeOr->getChild(0));
		Node * notB = m_factory.createNodeNot(nodeOr->getChild(1));
		nodeOr->setChild(0, NULL);
		nodeOr->setChild(1, NULL);

		nodeNot.reset(m_factory.createNodeAnd(notA, notB));
		return true;
		}

	// ~~A -> A
	inline bool MatchNotNot(std::auto_ptr<Node> & nodeNot, Int2Type<INPLASE>)
	{
		// Check the passed node type
		if(NT_NOT != nodeNot->getNodeType())
			return false;

		// Check the child node type
		Node * child = nodeNot->getChild(0);
		if(NT_NOT != child->getNodeType())
			return false;

		// Rewrite node
		Node * a = child->getChild(0);
		child->setChild(0, NULL);
		nodeNot.reset(a);
		return true;
	}

	// (A & B) | C -> (A & C) | (B & C)
	inline bool MatchOrAnd1(std::auto_ptr<Node> & nodeOr, Int2Type<INPLASE>)
	{
		// Check the processing type
		if(DNF != m_type)
			return false;

		// Check the passed node type
		if(NT_OR != nodeOr->getNodeType())
			return false;

		// Check the child node type
		Node * nodeAnd = nodeOr->getChild(0);
		if(NT_AND != nodeAnd->getNodeType())
			return false;

		// Rewrite node
		Node * c = nodeOr->getChild(1);
		nodeOr->setChild(1, m_factory.createNodeAnd(nodeAnd->getChild(1), c->clone())); // (A & B) | C -> (A & B) | (B & C)
		nodeAnd->setChild(1, c); // (A & B) | (B & C) -> (A & C) | (B & C)
		return true;
	}

	// A | (B & C) -> (A & B) | (A & C)
	inline bool MatchOrAnd2(std::auto_ptr<Node> & nodeOr, Int2Type<INPLASE>)
	{
		// Check the processing type
		if(DNF != m_type)
			return false;

		// Check the passed node type
		if(NT_OR != nodeOr->getNodeType())
			return false;

		// Check the child node type
		Node * nodeAnd = nodeOr->getChild(1);
		if(NT_AND != nodeAnd->getNodeType())
			return false;

			// Rewrite node
		Node * a = nodeOr->getChild(0);

		nodeOr->setChild(0, m_factory.createNodeAnd(a, nodeAnd->getChild(0))); // A | (B & C) -> (A & B) | (B & C)
		nodeAnd->setChild(0, a->clone()); // (A & B) | (B & C) -> (A & B) | (A & C)
		return true;
	}

	// (A | B) & C -> (A | C) & (B | C)
	inline bool MatchAndOr1(std::auto_ptr<Node> & nodeAnd, Int2Type<INPLASE>)
	{
		// Check the processing type
		if(CNF != m_type)
			return false;

		// Check the passed node type
		if(NT_AND != nodeAnd->getNodeType())
			return false;

		// Check the child node type
		Node * nodeOr = nodeAnd->getChild(0);
		if(NT_OR != nodeOr->getNodeType())
			return false;

		// Rewrite node
		Node * c = nodeAnd->getChild(1);
		nodeAnd->setChild(1, m_factory.createNodeOr(nodeOr->getChild(1), c->clone())); // (A | B) & C -> (A | B) & (B | C)
		nodeOr->setChild(1, c); // (A | B) & (B | C) -> // (A | C) & (B | C)
		return true;
	}

	// A & (B | C) -> (A | B) | (A | C)
	inline bool MatchAndOr2(std::auto_ptr<Node> & nodeAnd, Int2Type<INPLASE>)
	{
		// Check the processing type
		if(CNF != m_type)
			return false;

		// Check the passed node type
		if(NT_AND != nodeAnd->getNodeType())
			return false;

		// Check the child node type
		Node * nodeOr = nodeAnd->getChild(1);
		if(NT_OR != nodeOr->getNodeType())
			return false;

		// Rewrite node
		Node * a = nodeAnd->getChild(0);
		nodeAnd->setChild(0, m_factory.createNodeOr(a, nodeOr->getChild(0))); // A & (B | C) -> (A | B) & (B | C)
		nodeOr->setChild(0, a->clone()); // (A | B) & (B | C) -> (A | B) & (A | C)
		return true;
	}

public:
	bool operator()(std::auto_ptr<Node> & node)
	{
		enum { processAlgo = (Node::isStatic)? 0 : 1 };
		return MatchNotAnd(node, Int2Type<processAlgo>())||
			   MatchNotOr(node,  Int2Type<processAlgo>())||
			   MatchNotNot(node, Int2Type<processAlgo>())||
			   MatchOrAnd1(node, Int2Type<processAlgo>())||
			   MatchOrAnd2(node, Int2Type<processAlgo>())||
			   MatchAndOr1(node, Int2Type<processAlgo>())||
			   MatchAndOr2(node, Int2Type<processAlgo>());

	}
};

